| 1. Identificação | ||||||||||
| Tipo de Referência | Tese ou Dissertação (Thesis) | |||||||||
| Site | mtc-m21b.sid.inpe.br | |||||||||
| Código do Detentor | isadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S | |||||||||
| Identificador | 8JMKD3MGP3W34P/3K7T2BB | |||||||||
| Repositório | sid.inpe.br/mtc-m21b/2015/09.08.18.24 | |||||||||
| Última Atualização | 2016:02.17.17.42.53 (UTC) administrator | |||||||||
| Repositório de Metadados | sid.inpe.br/mtc-m21b/2015/09.08.18.24.45 | |||||||||
| Última Atualização dos Metadados | 2018:06.04.02.55.39 (UTC) administrator | |||||||||
| Chave Secundária | INPE-17619-TDI/2385 | |||||||||
| Chave de Citação | Santos:2015:MeApFo | |||||||||
| Título | A methodology to apply formal verification to UML-based software  | |||||||||
| Título Alternativo | Uma metodologia para aplicar verificação formal a software desenvolvido de acordo com UML | |||||||||
| Curso | CAP-COMP-SPG-INPE-MCTI-GOV-BR | |||||||||
| Ano | 2015 | |||||||||
| Data | 2015-10-02 | |||||||||
| Data de Acesso | 08 maio 2024 | |||||||||
| Tipo da Tese | Tese (Doutorado em Computação Aplicada) | |||||||||
| Tipo Secundário | TDI | |||||||||
| Número de Páginas | 196 | |||||||||
| Número de Arquivos | 1 | |||||||||
| Tamanho | 7737 KiB | |||||||||
| 2. Contextualização | ||||||||||
| Autor | Santos, Luciana Brasil Rebelo dos | |||||||||
| Banca | Carvalho, Solon Venâncio de (presidente) Santiago Júnior, Valdivino Alexandre de (orientador) Vijaykumar, Nandamudi Lankalapalli (orientador) Silveira, Fábio Fagundes Yano, Edgar Toshiro | |||||||||
| Endereço de e-Mail | lurebelo@gmail.com | |||||||||
| Universidade | Instituto Nacional de Pesquisas Espaciais (INPE) | |||||||||
| Cidade | São José dos Campos | |||||||||
| Histórico (UTC) | 2015-09-08 18:25:10 :: lurebelo -> administrator :: 2015-09-09 10:08:30 :: administrator -> yolanda :: 2015-09-14 13:09:46 :: yolanda -> lurebelo :: 2015-11-15 23:32:51 :: lurebelo -> administrator :: 2015-11-17 13:50:31 :: administrator -> yolanda :: 2016-02-17 17:45:55 :: yolanda -> marcelo.pazos@sid.inpe.br :: 2016-02-29 17:45:31 :: marcelo.pazos@sid.inpe.br :: -> 2015 2016-02-29 18:46:56 :: marcelo.pazos@sid.inpe.br -> administrator :: 2015 2018-06-04 02:55:39 :: administrator -> :: 2015 | |||||||||
| 3. Conteúdo e estrutura | ||||||||||
| É a matriz ou uma cópia? | é a matriz | |||||||||
| Estágio do Conteúdo | concluido | |||||||||
| Transferível | 1 | |||||||||
| Palavras-Chave | UML formal verification model checking SOLIMVA formal methods verificação formal métodos formais | |||||||||
| Resumo | Software development organizations aim to add quality to the created products, especially those dealing with critical systems, which require high quality software. Formal Methods offer a large potential to provide more effective verification techniques. Besides, Formal Verification methods, such as Model Checking, are best applied in early stages of system design, when costs are low and benefits can be high, increasing the quality of systems. Unified Modeling Language (UML) is widely used for modeling (object-oriented) software, and its use is increasing in the aerospace industry. Verification and Validation of complex software developed according to UML is not trivial due to complexity of the software itself, and the several different UML models/diagrams that can be used to model behavior and structure of the software. This PhD thesis presents an extension of a methodology called SOLIMVA, initially developed to generate model-based system and acceptance test cases considering Natural Language requirements artifacts (SOLIMVA 1.0), and to detect incompleteness in software specifications by means of Model Checking (SOLIMVA 2.0). Such an extension generated SOLIMVA 3.0 which transforms up to three different UML behavioral diagrams (sequence, behavioral state machine, and activity) into a single Transition System to support Model Checking of software developed in accordance with UML. In SOLIMVA 3.0, properties are formalized based on use case models or requirements expressed in pure textual notation. The translation into the Transition System is done for the NuSMV model checker, but there is a possibility in using other model checkers, such as SPIN. A tool, XML Metadata Interchange to Transition System (XMITS), was developed to automate some steps of SOLIMVA 3.0 methodology. The approach was applied to two real case studies (embedded software) related to project under development at Instituto Nacional de Pesquisas Espaciais (INPE). Defects were detected within the design of these software systems showing the feasibility of the methodology. The main contribution of this PhD thesis is the transformation of a non-formal language (UML) to a formal language (language of the NuSMV model checker) towards a greater adoption in practice of Formal Methods in software development. RESUMO: Organizações que desenvolvem software objetivam produzir produtos de software de qualidade, especialmente aquelas que lidam com sistemas críticos, que demandam software de alta qualidade. Métodos Formais oferecem grande potencial para prover técnicas de verificação mais efetivas. Além disso, métodos de Verificação Formal, como Model Checking, são aplicados de maneira mais eficiente nos estágios iniciais do projeto de software, quando os custos ainda são baixos e os benefícios podem ser altos, aumentando a qualidade dos sistemas de software. A Linguagem de Modelagem Unificada (UML) é consideravelmente utilizada para modelar software (orientado a objetos), e seu uso tem crescido na indústria aeroespacial. Verificação e Validação de sistemas complexos desenvolvidos de acordo com UML não são tarefas triviais, devido à complexidade do software em si, e a diversos diagramas/modelos UML diferentes que podem ser usados para modelar o comportamento e a estrutura do sistema. Esta tese de doutorado apresenta uma extensão de uma metodologia chamada SOLIMVA, desenvolvida inicialmente para gerar casos de teste de sistema e de aceitação baseados em modelos, considerando requisitos em Linguagem Natural (SOLIMVA 1.0), e para detectar não completude em especificações de software utilizando Model Checking (SOLIMVA 2.0). Tal extensão gerou a SOLIMVA 3.0, a qual transforma até três diferentes diagramas comportamentais da UML (sequência, atividades e máquina de estado) em um único Sistema de Transição de Estados para possibilitar a aplicação de Model Checking em software desenvolvido de acordo com a UML. Na SOLIMVA 3.0, as propriedades são formalizadas baseando-se nos modelos de casos de uso ou em requisitos expressos em notação textual pura. A tradução para o Sistema de Transição de Estados é feita para a ferramenta de Model Checking NuSMV, mas existe a possibilidade de se utilizar outras ferramentas, como por exemplo, SPIN. Uma ferramenta, XML Metadata Interchange to Transition System (XMITS), foi desenvolvida para automatizar algumas atividades da metodologia SOLIMVA 3.0. A abordagem foi aplicada em dois estudos de caso reais (software embarcado) relacionados a um projeto em desenvolvimento no Instituto Nacional de Pesquisas Espaciais (INPE). Foram encontrados defeitos nos projetos desses sistemas de software, mostrando a viabilidade da metodologia. A principal contribuição desta tese de doutorado é a transformação de uma linguagem não formal (UML) para uma linguagem formal (linguagem de entrada da ferramenta de Model Checking NuSMV), tendo como objetivo uma maior utilização, na prática, de Métodos Formais no processo de desenvolvimento de software. | |||||||||
| Área | COMP | |||||||||
| Arranjo | urlib.net > BDMCI > Fonds > Produção pgr ATUAIS > CAP > A methodology to... | |||||||||
| Conteúdo da Pasta doc | acessar | |||||||||
| Conteúdo da Pasta source |
| |||||||||
| Conteúdo da Pasta agreement |
| |||||||||
| 4. Condições de acesso e uso | ||||||||||
| URL dos dados | http://urlib.net/ibi/8JMKD3MGP3W34P/3K7T2BB | |||||||||
| URL dos dados zipados | http://urlib.net/zip/8JMKD3MGP3W34P/3K7T2BB | |||||||||
| Idioma | en | |||||||||
| Arquivo Alvo | publicacao.pdf | |||||||||
| Grupo de Usuários | administrator lurebelo marcelo.pazos@inpe.br yolanda.souza@mcti.gov.br | |||||||||
| Grupo de Leitores | administrator lurebelo marcelo.pazos@inpe.br yolanda.souza@mcti.gov.br | |||||||||
| Visibilidade | shown | |||||||||
| Licença de Direitos Autorais | urlib.net/www/2012/11.12.15.10 | |||||||||
| Detentor da Cópia | SID/SCD | |||||||||
| Permissão de Leitura | allow from all | |||||||||
| Permissão de Atualização | não transferida | |||||||||
| 5. Fontes relacionadas | ||||||||||
| Repositório Espelho | sid.inpe.br/mtc-m21b/2013/09.26.14.25.22 | |||||||||
| Unidades Imediatamente Superiores | 8JMKD3MGPCW/3F2PHGS | |||||||||
| Lista de Itens Citando | ||||||||||
| Acervo Hospedeiro | sid.inpe.br/mtc-m21b/2013/09.26.14.25.20 | |||||||||
| 6. Notas | ||||||||||
| Campos Vazios | academicdepartment affiliation archivingpolicy archivist callnumber contenttype creatorhistory descriptionlevel dissemination doi electronicmailaddress format group isbn issn label lineage mark nextedition notes number orcid parameterlist parentrepositories previousedition previouslowerunit progress resumeid rightsholder schedulinginformation secondarydate secondarymark session shorttitle sponsor subject tertiarymark tertiarytype url versiontype | |||||||||